Nuprl Lemma : CV_wf
0,22
postcript
pdf
A
:Type,
F
:(
t
:
(
t
A
)
A
). CV(
F
)
A
latex
Definitions
i
j
<
k
,
P
&
Q
,
A
B
,
A
,
False
,
i
j
,
P
Q
,
x
:
A
.
B
(
x
)
,
,
t
T
,
{
i
..
j
}
,
CV(
F
)
Lemmas
int
seg
wf
,
nat
wf
,
nat
properties
,
ge
wf
,
le
wf
,
subtype
rel
function
origin
A:Type, F:(t:
(tA)A). CV(F) 
A A:Type, F:(t:(tA)A). CV(F) A 
j < kB
A
j
Qx:A. B(x) T
}